Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:	app(perfectp,0)	→ false
2:	app(perfectp,app(s,x))	→ app(app(app(app(f,x),app(s,0)),app(s,x)),app(s,x))
3:	app(app(app(app(f,0),y),0),u)	→ true
4:	app(app(app(app(f,0),y),app(s,z)),u)	→ false
5:	app(app(app(app(f,app(s,x)),0),z),u)	→ app(app(app(app(f,x),u),app(app(minus,z),app(s,x))),u)
6:	app(app(app(app(f,app(s,x)),app(s,y)),z),u)	→ app(app(app(if,app(app(le,x),y)),app(app(app(app(f,app(s,x)),app(app(minus,y),x)),z),u)),app(app(app(app(f,x),u),z),u))

There are 25 dependency pairs:


7:	APP(perfectp,app(s,x))	→ APP(app(app(app(f,x),app(s,0)),app(s,x)),app(s,x))
8:	APP(perfectp,app(s,x))	→ APP(app(app(f,x),app(s,0)),app(s,x))
9:	APP(perfectp,app(s,x))	→ APP(app(f,x),app(s,0))
10:	APP(perfectp,app(s,x))	→ APP(f,x)
11:	APP(perfectp,app(s,x))	→ APP(s,0)
12:	APP(app(app(app(f,app(s,x)),0),z),u)	→ APP(app(app(app(f,x),u),app(app(minus,z),app(s,x))),u)
13:	APP(app(app(app(f,app(s,x)),0),z),u)	→ APP(app(app(f,x),u),app(app(minus,z),app(s,x)))
14:	APP(app(app(app(f,app(s,x)),0),z),u)	→ APP(app(f,x),u)
15:	APP(app(app(app(f,app(s,x)),0),z),u)	→ APP(f,x)
16:	APP(app(app(app(f,app(s,x)),0),z),u)	→ APP(app(minus,z),app(s,x))
17:	APP(app(app(app(f,app(s,x)),0),z),u)	→ APP(minus,z)
18:	APP(app(app(app(f,app(s,x)),app(s,y)),z),u)	→ APP(app(app(if,app(app(le,x),y)),app(app(app(app(f,app(s,x)),app(app(minus,y),x)),z),u)),app(app(app(app(f,x),u),z),u))
19:	APP(app(app(app(f,app(s,x)),app(s,y)),z),u)	→ APP(app(if,app(app(le,x),y)),app(app(app(app(f,app(s,x)),app(app(minus,y),x)),z),u))
20:	APP(app(app(app(f,app(s,x)),app(s,y)),z),u)	→ APP(if,app(app(le,x),y))
21:	APP(app(app(app(f,app(s,x)),app(s,y)),z),u)	→ APP(app(le,x),y)
22:	APP(app(app(app(f,app(s,x)),app(s,y)),z),u)	→ APP(le,x)
23:	APP(app(app(app(f,app(s,x)),app(s,y)),z),u)	→ APP(app(app(app(f,app(s,x)),app(app(minus,y),x)),z),u)
24:	APP(app(app(app(f,app(s,x)),app(s,y)),z),u)	→ APP(app(app(f,app(s,x)),app(app(minus,y),x)),z)
25:	APP(app(app(app(f,app(s,x)),app(s,y)),z),u)	→ APP(app(f,app(s,x)),app(app(minus,y),x))
26:	APP(app(app(app(f,app(s,x)),app(s,y)),z),u)	→ APP(app(minus,y),x)
27:	APP(app(app(app(f,app(s,x)),app(s,y)),z),u)	→ APP(minus,y)
28:	APP(app(app(app(f,app(s,x)),app(s,y)),z),u)	→ APP(app(app(app(f,x),u),z),u)
29:	APP(app(app(app(f,app(s,x)),app(s,y)),z),u)	→ APP(app(app(f,x),u),z)
30:	APP(app(app(app(f,app(s,x)),app(s,y)),z),u)	→ APP(app(f,x),u)
31:	APP(app(app(app(f,app(s,x)),app(s,y)),z),u)	→ APP(f,x)

The approximated dependency graph contains one SCC: {12-14,16,18,19,21,23,24,26,28-30}.

Consider the SCC {12-14,16,18,19,21,23,24,26,28-30}. By taking the AF π with π(app) = π(APP) = 1 together with the lexicographic path order with precedence perfectp ≻ f ≻ false, f ≻ if, f ≻ le, f ≻ minus and f ≻ true, the rules in {5,12-14,23,24,28-30} are weakly decreasing and the rules in {1-4,6,16,18,19,21,26} are strictly decreasing. There is one new SCC.
- Consider the SCC {12-14,23,24,28-30}. By taking the AF π with π(APP) = 1 and π(app) = [1] together with the lexicographic path order with precedence perfectp ≻ f ≻ app ≻ if, f ≻ false and f ≻ true, the rules in {5,12,23,28} are weakly decreasing and the rules in {1-4,6,13,14,24,29,30} are strictly decreasing. There is one new SCC.
  - Consider the SCC {12,23,28}. The constraints could not be solved.

Tyrolean Termination Tool (84.86 seconds) --- May 4, 2006